switch to APPEND;
SHOW PROOF;

SHOW PROOF 29:36;
REWRITE 32: BY SEXPSS∪{APPEND_UU_V,H_ASSAPP};
REWRITE 32: BY SEXPSS∪{APPEND_DEF,H_ASSAPP};